Iof proof for Lemma fast-fib:
1. f :
1.
n, a, b:
.
1. {m:
|
1. {
k:. (a = fib(k)) 
((k 
0) (b = 0)) ((0 < k) (b = fib(k - 1))) (m = fib(n+k))}
2. n :
3. v :
3. {m:
|
3. {
k:. (1 = fib(k)) ((k 0) (0 = 0)) ((0 < k) (0 = fib(k - 1))) (m = fib(n+k))}
4. f(n,1,0) = v
v = fib(n)
by D (-2)
1:
1: 3. v :
1: 4. k:.
1: 4. (1 = fib(k)) ((k 0) (0 = 0)) ((0 < k) (0 = fib(k - 1))) (v = fib(n+k))
1: 5. f(n,1,0) = v
1: v = fib(n)
.